import sys
import csv

def csv_to_list_of_dict(csv_file):
    result = []
    
    with open(csv_file, 'r') as file:
        reader = csv.DictReader(file)
        for row in reader:
            modified_row = {key.strip(): value.strip() for key, value in row.items()}
            result.append(modified_row)
    
    return result

def parseFilename(filename):
    # print(filename)
    if filename.find("nowholeDFA") != -1:
        return "nowholeDFA"
    if filename.find("lisa") != -1:
        return "lisa"
    if "tople" in filename:
        return "tople"
    if "SATtrace-guided-searchWholeDFA" in filename:
        return "combine-SATtraceDFA"
    if "mergeSort-opt" in filename:
        return "combine-mergeSort"
    if "fixLoopUnrealizable-removeCleanAll" in filename:
        return "combine-fixLoopRC"
    if "fixLoopUnrealizable" in filename:
        return "combine-fixLoop"
    if "ltlfsyn-combine" in filename:
        return "combine"
    if "ltlfsyn-raw-fixTarjan" in filename:
        return "raw-fixTarjan"
    if "old_ltlfsyn" in filename:
        return "old_ltlfsyn"
    if "ltlfsyn" in filename:
        return "ltlfsyn"
    if "nike" in filename:
        return "nike"
    if "cynthia" in filename:
        return "cynthia"
    if "lydia" in filename:
        return "lydia"
    if "copy" in filename:
        return "copy"
    if "svs" in filename:
        return "svs"
    if "sys" in filename:
        return "sys"
    if "bro2" in filename:
        return "bro2"
    return filename

if len(sys.argv) < 3:
    print("Please input two or more files!")
    sys.exit(1)

files = sys.argv[1:]
data_arr = []

file_num = len(files)
base_len = len(csv_to_list_of_dict(files[0]))

uni_solved = {}
for file in files:
    uni_solved[parseFilename(file)]=[]
    data = csv_to_list_of_dict(file)
    if len(data) != base_len:
        raise ValueError(file + ":\t lines of this file is not the same as others!")
    data_arr.append(data)


for i in range(base_len):
    solved_num = 0
    _solved_file = ''
    _result = ''
    _folder = ''
    _filename = ''
    for j in range(file_num):
        data = data_arr[j]
        result = data[i]['Result']
        folder = data[i]['Folder']
        filename = data[i]['Filename']
        if result == 'Unrealizable' or result == 'Realizable':
            # print(result)
            solved_num += 1
            _solved_file = files[j]
            _result = result
            _folder = folder
            _filename = filename
    # print(solved_num)
    if solved_num == 1:
        _tmp_dict = {}
        _tmp_dict["result"]=_result
        _tmp_dict["folder"]=_folder
        _tmp_dict["filename"]=_filename
        # uni_solved[parseFilename(_solved_file)].append({_result, _folder, _filename})
        uni_solved[parseFilename(_solved_file)].append(_tmp_dict)
        # print(parseFilename(_solved_file), _result, _folder, _filename, sep='\t')

for file in files:
    print(parseFilename(file), len(uni_solved[parseFilename(file)]))
print()
for file in files:
    print(parseFilename(file), ':')
    _uni_solved = uni_solved[parseFilename(file)]
    for item in _uni_solved:
        # _result, _folder, _filename = item
        _result = item["result"]
        _folder = item["folder"]
        _filename = item["filename"]
        # print('\t', _folder+'/'+_filename, '\t\t', _result)
        print("\t{:<36}{}".format(_folder+'/'+_filename, _result))
